 
  ///////////////////   BUILD PROOF  ///////////////////////////////////

 /**
  * @param expression: an Expression, which is to be matched
  * @param template: the Expression against which we will match
  * @param oldElements: variables potentially in the template whose
  *        corresponding elements in the expression we have previously
  *        identified.
  * @param kinds: a dictionary of Kinds (e.g. 'constant', 'prefix_function')
  *        which is used to determine whether an operator can be matched
  *        against. e.g. r&s matches p&q because the p and q represent
  *        arbitrary atoms, but r|s does not because & is not arbitrary and 
  *        must be matched exactly.
  * @result a dictionary extending oldElements, that for new operators in
  *         template gives the corresponding operator in expression.
  * e.g. A(x)&t, p&q, {} will return {p: A(x), q:t}
  * e.g. A(x)&t, p&q, {q: s} will throw an error
  * e.g. $y.R(y), $x.p, {} will return {x:y, p: R(y)} as dummies also matched
  */
  var matchExpression = function(expression, template, oldElements, kinds) {
    elements = {};
    for (var key in oldElements) {
      elements[key] = oldElements[key];
    }
    if (kinds[template.kind].matchable) {
      if (elements.hasOwnProperty(template.operator)) {
        if (checkExpressionsAreEqual(expression, elements[template.operator])) {
          return elements;
        } else {
          throw new UserError('unmatched_line', {});
        }
      } else {
        elements[template.operator] = expression;
        return elements;
      }
    } else {
      if (expression.operator !== template.operator ||
          expression.kind !== template.kind ||
          expression.arguments.length !== template.arguments.length ||
          expression.dummies.length !== template.dummies.length) {
          throw new UserError('unmatched_line', {});
      } else {
        return matchExpressionArray(
          expression.arguments.concat(expression.dummies), 
          template.arguments.concat(template.dummies), elements, kinds);
      }
    }
  };
  
  // companion of matchExpression
  var matchExpressionArray = function(array, templateArray, elements, kinds) {
    for (var i = 0; i < array.length; i++) {
      elements = matchExpression(array[i], templateArray[i], elements, kinds);
    }
    return elements;
  };

 /**
  * @param expression: an Expression into which we are substituting, e.g. x=y
  * @param substitutions: a dictionary of {string: Expression} specifying the
  *        substitions to perform (simultaneously), e.g {x:2, y:a+b}
  * @result the substituted Expression, e.g. 2=a+b
  */
  var substituteIntoExpression = function (expression, substitutions) {
    // we ignore substitutions for dummy variables
    var newSubstitutions = {};
    for (key in substitutions) {
      var isDummy = false;
      for (var i = 0; i < expression.dummies.length; i++) {
        if (expression.dummies[i].operator === key) {
          isDummy = true;
        } 
      }
      if (!isDummy) {
        newSubstitutions[key] = substitutions[key];
      }
    }
    if (substitutions.hasOwnProperty(expression.operator)) {
      return substitutions[expression.operator];
    } else {
      var output = {
        operator: expression.operator,
        kind: expression.kind,
        arguments: substituteIntoExpressionArray(expression.arguments, newSubstitutions),
        dummies: substituteIntoExpressionArray(expression.dummies, newSubstitutions)
      };
      if (expression.hasOwnProperty('type')) {
        output['type'] = expression['type'];
      }
      return output;
    }
  };

  // companion to substituteIntoExpression
  var substituteIntoExpressionArray = function(array, substitutions) {
    var output = [];
    for (var i = 0; i < array.length; i++) {
      output.push(substituteIntoExpression(array[i], substitutions));
    }
    return output;
  };


  // Replaces all operators from expression (including dummies) that appear in
  // elements with their entries in elements.
  var instantiateExpression = function(expression, elements) {
    if (elements.hasOwnProperty(expression.operator)) {
      return elements[expression.operator];
    } else {
      var output = {
        operator: expression.operator,
        kind: expression.kind,
        arguments: instantiateExpressionArray(expression.arguments, elements),
        dummies: instantiateExpressionArray(expression.dummies, elements)
      }
      if (expression.hasOwnProperty('type')) {
        output['type'] = expression.type;
      }
      return output;
    }
  };

  var instantiateExpressionArray = function(array, elements) {
    var output = [];
    for (var i = 0; i < array.length; i++) {
      output.push(instantiateExpression(array[i], elements));
    }
    return output;
  };

 /**
  * @param template: an ExpressionTemplate
  * @param elements: a dictionary of {string: Expression}
  * @return: an Expression
  */
  var computeExpressionFromTemplate =function(template, elements) {
    // e.g. template represents p[x -> a] and elements represents {p:A(y), x: y, a:2}
    var newExpression = instantiateExpression(template.expression, elements);
    var newSubstitutions = [];
    for (var i = 0; i < template.substitutions.length; i++) {
      newSubstitutions.push({});
      for (var key in template.substitutions[i]) {
        newSubstitutions[i][elements[key].operator] = instantiateExpression(template.substitutions[i][key], elements);
      }
    }
    // e.g. now new_expression is A(y) and new_subsitutions represents [y -> 2]
    for (var i = 0; i < newSubstitutions.length; i++) {
      newExpression = substituteIntoExpression(newExpression, newSubstitutions[i]);
    }
    return newExpression;
    // e.g. result is A(2)    
  };

  var computeExpressionsFromTemplateArray = function(templateArray, elements) {
    var output = [];
    for (var i = 0; i < templateArray.length; i++) {
      output.push(computeExpressionFromTemplate(templateArray[i], elements));
    }
    return output;
  }

 /**
  * @param messages: an array of LineMessages, each of which describes the
  *        mistake the student has made by writing this sort of line.
  * @param elements: a {string: Expression} dictionary deduced from comparing
  *        the line the student actually wrote to the LineTemplate provided by
  *        the techer of which it is an instance.
  * @param operators: from the student Language and used for display purposes.
  * This function throws a UserError (with the 'pre-rendered' code) that 
  * contains an array of strings describing the error, one of which will be 
  * chosen later to show to the student. If the messages list is empty 
  * (signifying that the line in question is a correct one) we return blank.
  */
  var renderLineMessages = function(messages, elements, operators) {
    if (messages.length > 0) {
      var renderedMessages = [];
      for (var j = 0; j < messages.length; j++) {
        renderedMessages.push('');
        for (var i = 0; i < messages[j].length; i++) {
          if (messages[j][i].format === 'string') {
            renderedMessages[j] += messages[j][i].content;
          } else {
            renderedMessages[j] += displayExpression(computeExpressionFromTemplate(messages[j][i].content, elements), operators);
          }
        }
      }
      throw new UserError('pre-rendered', {}, renderedMessages);
    }
  }

 /**
  * Checks whether protoLine is an instance of template, in terms of both
  * expressions and phrases.
  * @param protoLine: a ProtoLine, that is an array of phrases and expressions
  * @param template: the reader_view key of a LineTemplate, so an array of
  *        phrases and ExpressionTemplates.
  * @return a dictionary of the form {string: Expression} that specifies what
  *          each variable / atom in the template corresponds to in the
  *          protoLine.
  */
  var matchLineToTemplate = function(protoLine, template, kinds) {
    // These witness that the protoLine is an instance of the template. For
    // example if the protoLine is 'we know A&B' and the template is 'we know
    // p' then elements would end up as {p: A&B}.
    var elements = {};

    if (protoLine.length !== template.length) {
      throw new UserError('unmatched_line', {});
    }
    for (var i = 0; i < protoLine.length; i++) {
      if (protoLine[i].format !== template[i].format) {
        throw new UserError('unmatched_line', {});
      }
      if (protoLine[i].format === 'phrase' && protoLine[i].content !== template[i].content) {
        throw new UserError('unmatched_line', {});
      }
      if (protoLine[i].format === 'expression') {
        // only unsubstituted expression templates are useful in establishing the elements
        if (template[i].content.substitutions.length === 0) {
          elements = matchExpression(protoLine[i].content, template[i].content.expression, elements, kinds);
        }
      }
    }
    // now check the substituted expression templates agree
    for (var i = 0; i < protoLine.length; i++) {
      if (protoLine[i].format === 'expression' && template[i].content.substitutions.length > 0) {
        var expression = computeExpressionFromTemplate(template[i].content, elements)
        if (!checkExpressionsAreEqual(protoLine[i].content, expression)) {
          throw new UserError('unmatched_line', {});
        }
      }
    }
    return elements;
  };

 /**
  * This is used by buildLine. It checks that the types of the line are
  * correct and at the top agree with those the template requires, and 
  * likewise for the kinds of the line (if the template has an opinion).
  * @param elements: a dictionary of {string: Expression} that allows the line
  *        the student wrote to be deduced from the reader_view key of the
  *        LineTemplate in question.
  * @param templateReaderView: the reader_view key of a LineTemplate, so an array of 
  *        phrases and ExpressionTemplates.
  * @param language: a Language object giving the student language
  */
  var requireValidLine = function (elements, templateReaderView, language) {
    var arrayToCheck = [];
    var typesRequired = [];
    var kindErrors = [];
    for (var i = 0; i < templateReaderView.length; i++) {
      if (templateReaderView[i].format === 'expression') {
        var expression = computeExpressionFromTemplate(templateReaderView[i].content, elements);
        if (templateReaderView[i].content.hasOwnProperty('kind') && templateReaderView[i].content.kind !== expression.kind) {
          throw new UserError('wrong_kind_in_line', {expression: expression, expected_kind: templateReaderView[i].content.kind});
        }
        arrayToCheck.push(expression);
        typesRequired.push(templateReaderView[i].content.type);
      }
    }
    assignTypesToExpressionArray(arrayToCheck, typesRequired, language, ['variable']);
  };

 /**
  * @param lineString: a line of text written by the student
  * @param lineTemplates: an array of LineTemplates written by the teacher,
  *        that describe the sorts of lines a student might write; we try to 
  *        find one of which the given line is an instance.
  * @param language: the student language (a Language object)
  * @param vocabulary: the phrases available for the student to use. It is a 
  *        dictionary with entries like satisfying:['satisfying', 'such that']
  *        which indicates that the student can convey the concept of 
  *        'satsifying' by writing either 'satisfying' or 'such that'.
  * @return a Line object that is an abstract representation of the student's
  *          lineString, constructed from this string and one of the 
  *          lineTemplates.
  */
  var buildLine = function(lineString, lineTemplates, language, vocabulary) {
    // Get list of possible parsings of line (usually there is only one)
    var protoLines = parseLine(lineString, language.operators, vocabulary, false);
    // At this stage we wish to return the 'best' matching with the following
    // priority list:
    // 1. A valid matching to a 'correct' line template - i.e. one for a
    //    logically correct derivation. If we find one we return it immediately
    // 2. A valid matching to an incorrect line template
    // 3. An invalid matching to a line template
    var _isBetterAttempt = function(error1, error2) {
      return error2 === undefined || 
        (error1.code === 'pre-rendered' && !error2.code === 'pre-rendered') ||
        (error1.code !== 'unmatched_line' && error2.code === 'unmatched_line');
    }

    for (var i = 0; i < protoLines.results.length; i++) {
      for (var j = 0; j < lineTemplates.length; j++) {
        try {
          var elements = matchLineToTemplate(protoLines.results[i], lineTemplates[j].reader_view, language.kinds);
          requireValidLine(elements, lineTemplates[j].reader_view, language);
          renderLineMessages(lineTemplates[j].error, elements, language.operators);

          var antecedents = [];
          for (var k = 0; k < lineTemplates[j].antecedents.length; k++) {
            antecedents.push({
              format: 'expression',
              content: computeExpressionFromTemplate(lineTemplates[j].antecedents[k], elements)
            });
          }
          return {
            template: lineTemplates[j].name,
            elements: elements,
            antecedents: antecedents,
            results: computeExpressionsFromTemplateArray(lineTemplates[j].results, elements),
            variables: instantiateExpressionArray(lineTemplates[j].variables, elements),
            indentation: protoLines.indentation,
            text: lineString
          };
        }
        catch (err) {
          if (_isBetterAttempt(err, bestAttemptSoFar)) {
            var bestAttemptSoFar = err;
          }
        }
      }
    }
    throw bestAttemptSoFar;
  };

  // Only used for testing
  var displayLine = function(line, operators) {
    var elements = {};
    for (var key in line.elements) {
      elements[key] = displayExpression(line.elements[key], operators);
    }
    var antecedents = [];
    for (var i = 0; i < line.antecedents.length; i++) {
      antecedents.push(displayExpression(line.antecedents[i].content, operators));
    }
    return {
      template: line.template,
      elements: elements,
      antecedents: antecedents.join(', '),
      results: displayExpressionArray(line.results, operators),
      variables: displayExpressionArray(line.variables, operators),
      indentation: line.indentation,
      text: line.text
    }
  };

 /**
  * This is one of the two top-level student functions (with checkProof)
  * @param proofString: the proof as written by the student
  * @param widget: the widget_customization_args (originally written by the
  *        teacher) that are relevant to this problem.
  * @return a Proof object built from the given proofString, or {
  *            failure: a message describing something that went wrong
  *            line: the line in which the problem occurred (zero-indexed)
  *          }
  */
  var buildProof = function(proofString, widget) {
    var lineStrings = proofString.split('\n');
    var lines = [];
    for (var i = 0; i < lineStrings.length; i++) {
      try {
        lines.push(buildLine(lineStrings[i], widget.line_templates, widget.language, widget.vocabulary));
      }
      catch (err) {
        return {
          failure: renderError(err, widget.general_messages, widget.language),
          line: i
        };
      }
    }
    return {lines: lines};
  };

  // Only used for testing
  var displayProof = function(proof, operators) {
    var output = [];
    for (var i = 0; i < proof.lines.length; i++) {
      output.push(displayLine(proof.lines[i], operators));
    }
    return output;
  }

///////////////////   CHECK PROOF   ///////////////////////////////////////////

 /**
  * @param expression: the TypedExpression (in the control language) to be 
  *        evaluated, e.g. n+2
  * @param inputs: a dictionary with keys the free variables in the expression,
  *        giving for each the value they should be taken to have, e.g. {n:3}
  * @param model: a Model object that specifies how to evaluate functions - 
  *        e.g. that '+' should be interpreted as the usual addition.
  * @param parameters: these are sent to all of the EvaluationRules occurring
  *        in the model, for them to make use of if they wish. e.g. here they
  *        would include the student's proof, and the function 'num_lines' 
  *        would evaluate by examining this proof.
  * @param cache: expressions, at particular inputs, that were already
  *        evaluated.
  * @return the result of the expression with these inputs, e.g. 5
  */
  // NOTE: The code is ready for caching to be added to evaluate(). I believe
  // this would significantly speed up the code, but at the moment it is 
  // already fast enough so this is not a priority.
  // NOTE: the console.log here are used for testing
  var evaluate = function(expression, inputs, model, parameters, cache) {
    //// console.log('EVALUATE ' + displayExpression(expression, BASE_CONTROL_LANGUAGE.operators) + ' ' + JSON.stringify(inputs))
    if (expression.kind === 'variable') {
      var answer = inputs[expression.operator];
    } else if (expression.kind === 'constant') {
      var answer = expression.operator;
    } else {
      var evaluationRule = model.evaluation_rules[expression.operator];
      if (evaluationRule.format === 'top_down') {
        var answer =  evaluationRule.content(expression, inputs, model, parameters, cache);
      } else if (evaluationRule.format === 'definition') {
        // evaluate arguments (spec requires that the expression has no dummies)
        var newInputs = {};
        for (i = 0; i < expression.arguments.length; i++) {
          newInputs[evaluationRule.variables[i].operator] = evaluate(expression.arguments[i], inputs, model, parameters, cache);
        }
        var answer = evaluate(evaluationRule.content, newInputs, model, parameters, cache);
      } else if (evaluationRule.format === 'bottom_up') {
        // evaluate arguments (spec requires that there are no dummies)
        var arguments = [];
        for (i = 0; i < expression.arguments.length; i++) {
          var attempt = evaluate(expression.arguments[i], inputs, model, parameters, cache);
          // undefined is an error as above.
          if (attempt === undefined) {
            throw Error('evaluation failed');
          }
          arguments.push(attempt);
        }
        var types = [];
        for (var i = 0; i < expression.arguments.length; i++) {
          types.push(expression.arguments[i].type);
        }
        var answer =  evaluationRule.content(arguments, types, parameters);
      } else {
        throw Error('Unknown evaluation rule format (' + evaluationRule.format + ') sent to evaluate().')
      }
    }
    //// console.log(displayExpression(expression, BASE_CONTROL_LANGUAGE.operators) + ' ' + JSON.stringify(inputs) + ':  ' + JSON.stringify(answer));
    // An undefined result is for us equivalent to an error being thrown. We 
    // need to throw an error explicitely to avoid an undefined answer being
    // treated as 'false' by subsequent boolean operators.
    if (answer === undefined) {
      throw Error('evaluation failed');
    }
    return answer;
  };

 /**
  * @param mistake: a MistakeEntry that describes when a mistake occurs, and if
  *        so what to say to the student.
  * @param sectionName: the name of the section from which the mistake comes
  * @param lineNumber: the number of the line in the proof in which the mistake
  *        was made (zero-indexed)
  * @param model: a Model object providing information on how to evaluate
  *        functions the teacher may have used.
  * @param parameters: should be a dictionary of {
  *          proof: the student's proof in which the mistake was made
  *          assumptions: the assumptions allowed in the question
  *          target: what the student should prove (is widget.result[0])
  *        }
  * @param operators: from the student language, this is used to display
  *        expressions.
  * This function will take the ControlMessages given in the MistakeEntry and
  * evaluate them to get strings describing the problem that could be shown to
  * the student. It then throws a UserError containing these strings.
  */
  var renderControlMessage = function(mistake, sectionName, lineNumber, model, parameters, operators) {
    var renderedMessages = [];
    for (var j = 0; j < mistake.message.length; j++) {
      try {
        message = mistake.message[j];
        renderedMessage = '';
        for (var i = 0; i < message.length; i++) {
          if (message[i].format === 'string') {
            renderedMessage += message[i].content;
          } else {
            var rawResult = evaluate(message[i].content, {n:lineNumber+1}, model, parameters, {});
            renderedMessage += (message[i].content.type === 'set_of_formulas') ?
              displayExpressionArray(rawResult, operators):
              (message[i].content.type === 'formula') ?
                displayExpression(rawResult, operators):
                rawResult;
          }
        }
        renderedMessages.push(renderedMessage);
      }
      catch (err) {}
    }
    // If the teacher has made a mistake and none of the messages they have 
    // provided can be evaluated then we try to return to the student as 
    // helpful a message as possible.
    throw (renderedMessages.length > 0) ?
      new UserError('pre-rendered', {}, renderedMessages):
      new UserError('unspecified_mistake', {section: sectionName, entry: mistake.name});
  };

 /**
  * This is the second top-level function for the student.
  * @param proof: a Proof object constructed by buildProof()
  * @param widget: the widget_customization_args for this state
  * @return true if none of the mistakes in the widget.mistake_table have been
  *          made in the proof, otherwise  {
  *            failure: a description of the first mistake identified,
  *            line: the line the error occurred in (zero-indexed)
  *          }
  */
  var checkProof = function(proof, widget) {
    var cache = {};
    var parameters = {
      proof: proof,
      assumptions: widget.assumptions,
      target: widget.results[0]
    }
    for (var i = 0; i < widget.mistake_table.length; i++) {
      for (var line = 0; line < proof.lines.length; line++) {
        for (var j = 0; j < widget.mistake_table[i].entries.length; j++) {
          var mistake = widget.mistake_table[i].entries[j];
          // If the formula determining whether an error occurs cannot be
          // evaluated then the error is deemed not to have occurred. This is
          // so the teacher can write formulas like "indentation(n-1)" and have
          // it implicit that n>1.
          var check = false;
          try {var check = evaluate(mistake.occurs, {n: line+1}, widget.control_model, parameters, cache);}
          catch(err) {}
          if (check) {
            try {
              renderControlMessage(
                mistake, widget.mistake_table[i].name, line, widget.control_model, 
                parameters, widget.language.operators);
            }
            catch(err) {
              return {
                failure: renderError(err, widget.general_messages, widget.language),
                line: line
              };
            }
          }
        }
      }
    }
    return true;
  }